KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmp7nBdQU/bubblesort.xml









The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS


↳1 RenamingProof (⇔, 0 ms)


↳2 CpxRelTRS


↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


↳4 typed CpxTrs


↳5 OrderProof (LOWER BOUND(ID), 0 ms)


↳6 typed CpxTrs


↳7 RewriteLemmaProof (LOWER BOUND(ID), 450 ms)


↳8 BEST


    ↳9 typed CpxTrs


        ↳10 RewriteLemmaProof (LOWER BOUND(ID), 73 ms)


        ↳11 BEST


            ↳12 typed CpxTrs


            ↳13 typed CpxTrs


    ↳14 typed CpxTrs









(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))

len(Cons(x, xs)) → +(S(0), len(xs))

bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))

len(Nil) → 0

bubble(x, Nil) → Cons(x, Nil)

bsort(0, xs) → xs

bubblesort(xs) → bsort(len(xs), xs)

The (relative) TRS S consists of the following rules:

+(x, S(0)) → S(x)

+(S(0), y) → S(y)

<(S(x), S(y)) → <(x, y)

<(0, S(y)) → True

<(x, 0) → False

bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))

bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Rewrite Strategy: INNERMOST




(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))

len(Cons(x, xs)) → +'(S(0'), len(xs))

bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))

len(Nil) → 0'

bubble(x, Nil) → Cons(x, Nil)

bsort(0', xs) → xs

bubblesort(xs) → bsort(len(xs), xs)

The (relative) TRS S consists of the following rules:

+'(x, S(0')) → S(x)

+'(S(0'), y) → S(y)

<(S(x), S(y)) → <(x, y)

<(0', S(y)) → True

<(x, 0') → False

bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))

bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Rewrite Strategy: INNERMOST




(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(4) Obligation:
Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'




(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
bsort, bubble, len, <
They will be analysed ascendingly in the following order:
bubble < bsort
< < bubble




(6) Obligation:
Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
len, bsort, bubble, <
They will be analysed ascendingly in the following order:
bubble < bsort
< < bubble




(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
Induction Base:
len(gen_Cons:Nil4_0(0)) →RΩ(1)
0'
Induction Step:
len(gen_Cons:Nil4_0(+(n7_0, 1))) →RΩ(1)
+'(S(0'), len(gen_Cons:Nil4_0(n7_0))) →IH
+'(S(0'), gen_S:0'5_0(c8_0)) →RΩ(0)
S(gen_S:0'5_0(n7_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).




(8) Complex Obligation (BEST)




(9) Obligation:
Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
<, bsort, bubble
They will be analysed ascendingly in the following order:
bubble < bsort
< < bubble




(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) → True, rt ∈ Ω(0)
Induction Base:
<(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) →RΩ(0)
True
Induction Step:
<(gen_S:0'5_0(+(n417_0, 1)), gen_S:0'5_0(+(1, +(n417_0, 1)))) →RΩ(0)
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) →IH
True
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).




(11) Complex Obligation (BEST)




(12) Obligation:
Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) → True, rt ∈ Ω(0)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
bubble, bsort
They will be analysed ascendingly in the following order:
bubble < bsort




(13) Obligation:
Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) → True, rt ∈ Ω(0)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.




(14) Obligation:
Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.